$\forall$$E$:Type, ${\it pred?}$:($E$$\rightarrow$($E$+Unit)), $n$:$\mathbb{N}$, $a$, $j$:$E$.
\\[0ex]first($j$) $\Rightarrow$ rel\_exp($E$;$\lambda$$x$,$y$. $\neg$first($y$) \& $x$ $=$ pred($y$) $\in$ $E$;$n$)($a$,$j$) $\Rightarrow$ $a$ $=$ $j$